;;;===========================================================================
;;;
;;; Direct Sum Equivalence Theorem
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 24/05/10 || End date: 24/05/10
;;;
;;;===========================================================================


(in-package "ACL2")

(include-book "direct-sum-structure")

(encapsulate
 
 ;;**************************************************
 ;; Signaturas
 ;;**************************************************

 (
 ;;--------------------------------------------------
 ;; The signatures of the ring R
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-ring-Z *) => *)
 ;; Addition operation ring
 ((addition-ring-Z * *)=> *)
 ;; Product operation ring
 ((product-ring-Z * *) => *)
 ;; Inverse ring
 ((inverse-Z *) => *)
 ;; Zero element ring
 ((zero-element-Z ) => *)
 ;; Unit element ring
 ((unit-Z )=> *)

 ;;--------------------------------------------------
 ;; First homotopy equivalence C1 <<= D1 =>> H1
 ;;--------------------------------------------------

 ;;--------------------------------------------------
 ;; C1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-C1 * *) => *)
 ;; Group Operation 
 ((group-operation-C1 * * *) => *)
 ;; Zero element
 ((zero-C1 *) => *)
 ;; External multiplication
 ((external-C1 * * *) => *)
 ;; Inverse element
 ((inverse-C1 * *) => *)

 ;;--------------------------------------------------
 ;; The C1 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-C1 * *) => *)

 ;;--------------------------------------------------
 ;; D1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-D1 * *) => *)
 ;; Group Operation 
 ((group-operation-D1 * * *) => *)
 ;; Zero element
 ((zero-D1 *) => *)
 ;; External multiplication
 ((external-D1 * * *) => *)
 ;; Inverse element
 ((inverse-D1 * *) => *)

 ;;--------------------------------------------------
 ;; The D1 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-D1 * *) => *)

  ;;--------------------------------------------------
 ;; H1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-H1 * *) => *)
 ;; Group Operation 
 ((group-operation-H1 * * *) => *)
 ;; Zero element
 ((zero-H1 *) => *)
 ;; External multiplication
 ((external-H1 * * *) => *)
 ;; Inverse element
 ((inverse-H1 * *) => *)

 ;;--------------------------------------------------
 ;; The H1 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-H1 * *) => *)

 ;;--------------------------------------------------
 ;; Second homotopy equivalence C2 <<= D2 =>> H2
 ;;--------------------------------------------------


 ;;--------------------------------------------------
 ;; C2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-C2 * *) => *)
 ;; Group Operation 
 ((group-operation-C2 * * *) => *)
 ;; Zero element
 ((zero-C2 *) => *)
 ;; External multiplication
 ((external-C2 * * *) => *)
 ;; Inverse element
 ((inverse-C2 * *) => *)

 ;;--------------------------------------------------
 ;; The C2 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-C2 * *) => *)

 ;;--------------------------------------------------
 ;; D2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-D2 * *) => *)
 ;; Group Operation 
 ((group-operation-D2 * * *) => *)
 ;; Zero element
 ((zero-D2 *) => *)
 ;; External multiplication
 ((external-D2 * * *) => *)
 ;; Inverse element
 ((inverse-D2 * *) => *)

 ;;--------------------------------------------------
 ;; The D2 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-D2 * *) => *)

  ;;--------------------------------------------------
 ;; H2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-H2 * *) => *)
 ;; Group Operation 
 ((group-operation-H2 * * *) => *)
 ;; Zero element
 ((zero-H2 *) => *)
 ;; External multiplication
 ((external-H2 * * *) => *)
 ;; Inverse element
 ((inverse-H2 * *) => *)

 ;;--------------------------------------------------
 ;; The H2 differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-H2 * *) => *)

 
 ;;--------------------------------------------------
 ;; Morphisms of the first homotopy equivalence
 ;;--------------------------------------------------

 ;;--------------------------------------------------
 ;; The lf1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lf1 * *) => *)

 ;;--------------------------------------------------
 ;; The lg1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lg1 * *) => *)


 ;;--------------------------------------------------
 ;; The lh1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lh1 * *) => *)

 ;;--------------------------------------------------
 ;; The rf1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rf1 * *) => *)

 ;;--------------------------------------------------
 ;; The rg1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rg1 * *) => *)


 ;;--------------------------------------------------
 ;; The rh1 C1 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rh1 * *) => *)

 ;;--------------------------------------------------
 ;; The lf2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lf2 * *) => *)

 ;;--------------------------------------------------
 ;; The lg2 C2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lg2 * *) => *)


 ;;--------------------------------------------------
 ;; The lh2 C2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((lh2 * *) => *)

 ;;--------------------------------------------------
 ;; The rf2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rf2 * *) => *)

 ;;--------------------------------------------------
 ;; The rg2 C2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rg2 * *) => *)


 ;;--------------------------------------------------
 ;; The rh2 C2 morphism
 ;;--------------------------------------------------

 ;; The function
 ((rh2 * *) => *)

 
 )
 ;;**************************************************
 ;; Witnesses
 ;;**************************************************
 
 ;;--------------------------------------------------
 ;; The witnesses of the ring Z
 ;;--------------------------------------------------

 ;; The characteristic function

 (local (defun inv-ring-Z (a)
	  (integerp a)))
 
 ;; Addition operation Z
 (local (defun addition-ring-Z (a b)
	  (+ a b)))

 ;; Product operation ring
 (local (defun product-ring-Z (a b)
	  (* a b)))

 ;; Inverse addition
 (local (defun inverse-Z (a)
	  (- a)))

 ;; Zero element ring
 (local (defun zero-element-Z nil
	  0))

 ;; Unit element ring
 (local (defun unit-Z nil
	  1))

 ;;--------------------------------------------------
 ;; C1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-C1 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-C1 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-C1 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-C1 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-C1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The C1 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-C1 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; D1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-D1 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-D1 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-D1 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-D1 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-D1 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The D1 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-D1 (n a)
	  (declare (ignore n a))
	  0))

  ;;--------------------------------------------------
 ;; H1 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-H1 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-H1 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-H1 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-H1 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-H1 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The H1 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-H1 (n a)
	  (declare (ignore n a))
	  0))



 ;;--------------------------------------------------
 ;; C2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-C2 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-C2 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-C2 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-C2 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-C2 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The C2 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-C2 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; D2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-D2 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-D2 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-D2 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-D2 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-D2 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The D2 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-D2 (n a)
	  (declare (ignore n a))
	  0))


  ;;--------------------------------------------------
 ;; H2 Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-H2 (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-H2 (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-H2 (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-H2 (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-H2 (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The H2 differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-H2 (n a)
	  (declare (ignore n a))
	  0))
 


 ;;--------------------------------------------------
 ;; The lf1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lf1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The lg1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lg1 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lh1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lh1 (n a)
	  (declare (ignore n a))
	  0))


;;--------------------------------------------------
 ;; The rf1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rf1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The rg1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rg1 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The rh1 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rh1 (n a)
	  (declare (ignore n a))
	  0))



 ;;--------------------------------------------------
 ;; The lf2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lf2 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The lg2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lg2 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lh2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun lh2 (n a)
	  (declare (ignore n a))
	  0))


;;--------------------------------------------------
 ;; The rf2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rf2 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The rg2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rg2 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The lh2 morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun rh2 (n a)
	  (declare (ignore n a))
	  0))


  ;;************************************************** 
  ;; Properties
  ;;************************************************** 

(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-D1 'group-operation-D1 'zero-D1 'external-D1 'inverse-D1 'd-D1 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-C1 'group-operation-C1 'zero-C1 'external-C1 'inverse-C1 'd-C1 )
  'lf1  'lg1  'lh1
  )
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-D1 'group-operation-D1 'zero-D1 'external-D1 'inverse-D1 'd-D1 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-H1 'group-operation-H1 'zero-H1 'external-H1 'inverse-H1 'd-H1 )
  'rf1  'rg1  'rh1
  ))
 'homotopy-equivalence-1
   )


(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-D2 'group-operation-D2 'zero-D2 'external-D2 'inverse-D2 'd-D2 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-C2 'group-operation-C2 'zero-C2 'external-C2 'inverse-C2 'd-C2 )
  'lf2  'lg2  'lh2
  )
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-D2 'group-operation-D2 'zero-D2 'external-D2 'inverse-D2 'd-D2 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-H2 'group-operation-H2 'zero-H2 'external-H2 'inverse-H2 'd-H2 )
  'rf2  'rg2  'rh2
  ))
 'homotopy-equivalence-2
   )



)


;;==================================================
;; The Direct Sum definitions
;;==================================================

;;--------------------------------------------------
;; Direct Sum C1+C2
;;--------------------------------------------------

(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-C2 group-operation-C2 zero-C2 external-C2 inverse-C2 d-C2 C2
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-2-is-an-homotopy-equivalence|)))))

(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-C1 group-operation-C1 zero-C1 external-C1 inverse-C1 d-C1 C1
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|)))))


(defthm c1-c2-help1 (IMPLIES (AND (INV-C2 N A)
              (INV-C2 N B)
              (INV-C2 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C2 N A (GROUP-OPERATION-C2 N B C))
		(GROUP-OPERATION-C2 N C (GROUP-OPERATION-C2 N A B))
                )) 
:hints (("Goal" :use ((:instance |C2-is-a-chain-complex|)))))

(defthm c1-c2-help1-b (IMPLIES (AND (INV-C2 N A)
              (INV-C2 N B)
              (INV-C2 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C2 N A (GROUP-OPERATION-C2 N B C))
		(GROUP-OPERATION-C2 N b (GROUP-OPERATION-C2 N A c))
                )) 
:hints (("Goal" :use ((:instance c1-c2-help1)))))


(defthm c1-c2-help2 (IMPLIES (AND (INV-C1 N A)
              (INV-C1 N B)
              (INV-C1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C1 N A (GROUP-OPERATION-C1 N B C))
		(GROUP-OPERATION-C1 N C (GROUP-OPERATION-C1 N A B))
                )) 
:hints (("Goal" :use ((:instance |C1-is-a-chain-complex|)))))


(defthm c1-c2-help3 (IMPLIES (AND (INV-C1 N A)
              (INV-C1 N B)
              (INV-C1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-C1 N A (GROUP-OPERATION-C1 N B C))
		(GROUP-OPERATION-C1 N b (GROUP-OPERATION-C1 N A c))
                )) 
:hints (("Goal" :use ((:instance c1-c2-help2)))))


(defthm c1-c2-help4
	 (IMPLIES (AND (INV-C1 N A) (INTEGERP N))
		  (INV-C1 (+ N -1) (D-C1 N A)))
	 :hints (("Goal" :use ((:instance |C1-is-a-chain-complex|)))))
      
(defthm c1-c2-help5
	 (IMPLIES (AND (INV-C1 N A) (INTEGERP N))
		  (INV-C1 (+ -1 n) (D-C1 N A)))
	 :hints (("Goal" :use ((:instance c1-c2-help4)))))


(defthm c1-c2-help6
	 (IMPLIES (AND (INV-C2 N A) (INTEGERP N))
		  (INV-C2 (+ N -1) (D-C2 N A)))
	 :hints (("Goal" :use ((:instance |C2-is-a-chain-complex|)))))
      
(defthm c1-c2-help7
	 (IMPLIES (AND (INV-C2 N A) (INTEGERP N))
		  (INV-C2 (+ -1 n) (D-C2 N A)))
	 :hints (("Goal" :use ((:instance c1-c2-help6)))))

(definstance-*ds*
  ((inv-ring inv-ring-Z)
    (addition-ring addition-ring-Z)
    (product-ring product-ring-Z)
    (inverse inverse-Z)
    (zero-element zero-element-Z)
    (unit unit-Z)
    (inv-D inv-C2)
    (group-operation-D group-operation-C2)
    (zero-D zero-C2)
    (external-D external-C2)
    (inverse-D inverse-C2)
    (d-D d-C2)
    (inv-C inv-C1) 
    (group-operation-C group-operation-C1)
    (zero-C zero-C1)
    (external-C external-C1)
    (inverse-C inverse-C1)
    (d-C d-C1)    
    )
  "-ds-C1-C2")



;;--------------------------------------------------
;; Direct-sum D1+D2
;;--------------------------------------------------

(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-D2 group-operation-D2 zero-D2 external-D2 inverse-D2 d-D2 D2
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-2-is-an-homotopy-equivalence|)))))

(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-D1 group-operation-D1 zero-D1 external-D1 inverse-D1 d-D1 D1
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|)))))


(defthm d1-d2-help1 (IMPLIES (AND (INV-D2 N A)
              (INV-D2 N B)
              (INV-D2 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D2 N A (GROUP-OPERATION-D2 N B C))
		(GROUP-OPERATION-D2 N C (GROUP-OPERATION-D2 N A B))
                )) 
:hints (("Goal" :use ((:instance |D2-is-a-chain-complex|)))))

(defthm d1-d2-help1-b (IMPLIES (AND (INV-D2 N A)
              (INV-D2 N B)
              (INV-D2 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D2 N A (GROUP-OPERATION-D2 N B C))
		(GROUP-OPERATION-D2 N b (GROUP-OPERATION-D2 N A c))
                )) 
:hints (("Goal" :use ((:instance d1-d2-help1)))))


(defthm d1-d2-help2 (IMPLIES (AND (INV-D1 N A)
              (INV-D1 N B)
              (INV-D1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D1 N A (GROUP-OPERATION-D1 N B C))
		(GROUP-OPERATION-D1 N C (GROUP-OPERATION-D1 N A B))
                )) 
:hints (("Goal" :use ((:instance |D1-is-a-chain-complex|)))))


(defthm d1-d2-help3 (IMPLIES (AND (INV-D1 N A)
              (INV-D1 N B)
              (INV-D1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-D1 N A (GROUP-OPERATION-D1 N B C))
		(GROUP-OPERATION-D1 N b (GROUP-OPERATION-D1 N A c))
                )) 
:hints (("Goal" :use ((:instance d1-d2-help2)))))


(defthm d1-d2-help4
	 (IMPLIES (AND (INV-D1 N A) (INTEGERP N))
		  (INV-D1 (+ N -1) (D-D1 N A)))
	 :hints (("Goal" :use ((:instance |D1-is-a-chain-complex|)))))
      
(defthm d1-d2-help5
	 (IMPLIES (AND (INV-D1 N A) (INTEGERP N))
		  (INV-D1 (+ -1 n) (D-D1 N A)))
	 :hints (("Goal" :use ((:instance d1-d2-help4)))))


(defthm d1-d2-help6
	 (IMPLIES (AND (INV-D2 N A) (INTEGERP N))
		  (INV-D2 (+ N -1) (D-D2 N A)))
	 :hints (("Goal" :use ((:instance |D2-is-a-chain-complex|)))))
      
(defthm d1-d2-help7
	 (IMPLIES (AND (INV-D2 N A) (INTEGERP N))
		  (INV-D2 (+ -1 n) (D-D2 N A)))
	 :hints (("Goal" :use ((:instance d1-d2-help6)))))

(definstance-*ds*
  ((inv-ring inv-ring-Z)
    (addition-ring addition-ring-Z)
    (product-ring product-ring-Z)
    (inverse inverse-Z)
    (zero-element zero-element-Z)
    (unit unit-Z)
    (inv-D inv-D2)
    (group-operation-D group-operation-D2)
    (zero-D zero-D2)
    (external-D external-D2)
    (inverse-D inverse-D2)
    (d-D d-D2)
    (inv-C inv-D1) 
    (group-operation-C group-operation-D1)
    (zero-C zero-D1)
    (external-C external-D1)
    (inverse-C inverse-D1)
    (d-C d-D1)    
    )
  "-ds-D1-D2")



;;--------------------------------------------------
;; Direct Sum H1+H2
;;--------------------------------------------------



(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-H2 group-operation-H2 zero-H2 external-H2 inverse-H2 d-H2 H2
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-2-is-an-homotopy-equivalence|)))))

(defchain-complex inv-ring-Z addition-ring-Z zero-element-Z inverse-Z product-ring-Z unit-Z
	 inv-H1 group-operation-H1 zero-H1 external-H1 inverse-H1 d-H1 H1
	 :hints (("Goal" :use ((:instance |HOMOTOPY-EQUIVALENCE-1-is-an-homotopy-equivalence|)))))


(defthm h1-h2-help1 (IMPLIES (AND (INV-H2 N A)
              (INV-H2 N B)
              (INV-H2 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-H2 N A (GROUP-OPERATION-H2 N B C))
		(GROUP-OPERATION-H2 N C (GROUP-OPERATION-H2 N A B))
                )) 
:hints (("Goal" :use ((:instance |H2-is-a-chain-complex|)))))

(defthm h1-h2-help1-b (IMPLIES (AND (INV-H2 N A)
              (INV-H2 N B)
              (INV-H2 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-H2 N A (GROUP-OPERATION-H2 N B C))
		(GROUP-OPERATION-H2 N b (GROUP-OPERATION-H2 N A c))
                )) 
:hints (("Goal" :use ((:instance h1-h2-help1)))))


(defthm h1-h2-help2 (IMPLIES (AND (INV-H1 N A)
              (INV-H1 N B)
              (INV-H1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-H1 N A (GROUP-OPERATION-H1 N B C))
		(GROUP-OPERATION-H1 N C (GROUP-OPERATION-H1 N A B))
                )) 
:hints (("Goal" :use ((:instance |H1-is-a-chain-complex|)))))


(defthm h1-h2-help3 (IMPLIES (AND (INV-H1 N A)
              (INV-H1 N B)
              (INV-H1 N C)
	      (integerp n))
         (EQUAL (GROUP-OPERATION-H1 N A (GROUP-OPERATION-H1 N B C))
		(GROUP-OPERATION-H1 N b (GROUP-OPERATION-H1 N A c))
                )) 
:hints (("Goal" :use ((:instance h1-h2-help2)))))


(defthm h1-h2-help4
	 (IMPLIES (AND (INV-H1 N A) (INTEGERP N))
		  (INV-H1 (+ N -1) (D-H1 N A)))
	 :hints (("Goal" :use ((:instance |H1-is-a-chain-complex|)))))
      
(defthm h1-h2-help5
	 (IMPLIES (AND (INV-H1 N A) (INTEGERP N))
		  (INV-H1 (+ -1 n) (D-H1 N A)))
	 :hints (("Goal" :use ((:instance h1-h2-help4)))))


(defthm h1-h2-help6
	 (IMPLIES (AND (INV-H2 N A) (INTEGERP N))
		  (INV-H2 (+ N -1) (D-H2 N A)))
	 :hints (("Goal" :use ((:instance |H2-is-a-chain-complex|)))))
      
(defthm h1-h2-help7
	 (IMPLIES (AND (INV-H2 N A) (INTEGERP N))
		  (INV-H2 (+ -1 n) (D-H2 N A)))
	 :hints (("Goal" :use ((:instance h1-h2-help6)))))

(definstance-*ds*
  ((inv-ring inv-ring-Z)
    (addition-ring addition-ring-Z)
    (product-ring product-ring-Z)
    (inverse inverse-Z)
    (zero-element zero-element-Z)
    (unit unit-Z)
    (inv-D inv-H2)
    (group-operation-D group-operation-H2)
    (zero-D zero-H2)
    (external-D external-H2)
    (inverse-D inverse-H2)
    (d-D d-H2)
    (inv-C inv-H1) 
    (group-operation-C group-operation-H1)
    (zero-C zero-H1)
    (external-C external-H1)
    (inverse-C inverse-H1)
    (d-C d-H1)    
    )
  "-ds-H1-H2")



;;;--------------------------------------------------
;;; Morphisms of the equivalence
;;;--------------------------------------------------

(defun lf-ds (n a)
  (list (lf1 n (car a))
	(lf2 n (cadr a))))

(defun lg-ds (n a)
  (list (lg1 n (car a))
	(lg2 n (cadr a))))

(defun lh-ds (n a)
  (list (lh1 n (car a))
	(lh2 n (cadr a))))

(defun rf-ds (n a)
  (list (rf1 n (car a))
	(rf2 n (cadr a))))

(defun rg-ds (n a)
  (list (rg1 n (car a))
	(rg2 n (cadr a))))

(defun rh-ds (n a)
  (list (rh1 n (car a))
	(rh2 n (cadr a))))


;;;--------------------------------------------------
;;; Homotopy Equivalence Direct Sum
;;;--------------------------------------------------

(in-theory (disable COMMUTATIVITY-OF-+))

(defthm inv-d1-lh1
  (IMPLIES (AND (INV-D1 N a)
		(INTEGERP N))
         (INV-D1 (+ N 1) (LH1 N a))))


(defthm inv-d2-lh2
  (IMPLIES (AND (INV-D2 N a)
		(INTEGERP N))
         (INV-D2 (+ N 1) (LH2 N a))))



(defthm inv-d1-rh1
  (IMPLIES (AND (INV-D1 N a)
		(INTEGERP N))
         (INV-D1 (+ N 1) (rH1 N a))))


(defthm inv-d2-rh2
  (IMPLIES (AND (INV-D2 N a)
		(INTEGERP N))
         (INV-D2 (+ N 1) (rH2 N a))))

(in-theory (enable COMMUTATIVITY-OF-+))

(defthm inv-d1-lh1-bis
  (IMPLIES (AND (INV-D1 N a)
		(INTEGERP N))
         (INV-D1 (+ 1 n) (LH1 N a)))
  :hints (("Goal" :use (:instance inv-d1-lh1))))

(defthm inv-d2-lh2-bis
  (IMPLIES (AND (INV-D2 N a)
		(INTEGERP N))
         (INV-D2 (+ 1 n) (LH2 N a)))
  :hints (("Goal" :use (:instance inv-d2-lh2))))



(defthm inv-d1-rh1-bis
  (IMPLIES (AND (INV-D1 N a)
		(INTEGERP N))
         (INV-D1 (+ 1 n) (rH1 N a)))
  :hints (("Goal" :use (:instance inv-d1-rh1))))


(defthm inv-d2-rh2-bis
  (IMPLIES (AND (INV-D2 N a)
		(INTEGERP N))
         (INV-D2 (+ 1 n) (rH2 N a)))
  :hints (("Goal" :use (:instance inv-d2-rh2))))



(check-heq-p
(heq
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-ds-ds-d1-d2 'group-suspension-suspension-operation-D1 'zero-ds-ds-d1-d2 
   'external-ds-ds-d1-d2 'inverse-ds-ds-d1-d2 'd-ds-ds-d1-d2 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-ds-ds-c1-c2 'group-operation-ds-ds-c1-c2 'zero-ds-ds-c1-c2 'external-ds-ds-c1-c2 'inverse-ds-ds-c1-c2 'd-ds-ds-c1-c2 )
  'lf-ds  'lg-ds  'lh-ds
  )
 (reduction 
 (chain-complex 
  'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z 
   'inv-ds-ds-d1-d2 'group-operation-ds-ds-d1-d2 'zero-ds-ds-d1-d2 'external-ds-ds-d1-d2 'inverse-ds-ds-d1-d2 'd-ds-ds-d1-d2 )
 (chain-complex 
   'inv-ring-Z 'addition-ring-Z 'zero-element-Z 'inverse-Z 'product-ring-Z 'unit-Z
    'inv-ds-ds-h1-h2 'group-operation-ds-ds-h1-h2 'zero-ds-ds-h1-h2 'external-ds-ds-h1-h2 'inverse-ds-ds-h1-h2 'd-ds-ds-h1-h2 )
  'rf-ds  'rg-ds  'rh-ds
  ))
 'homotopy-equivalence-ds
   )

;;;===========================================================================
;;;
;;; End of the proof of the Direct Sum Equivalence Theorem
;;;
;;;===========================================================================

;;;----------------------------------------------------------------------------
;;; 
;;; Defining the generic theory:
;;;
;;;----------------------------------------------------------------------------


(include-book "generic-theory")


#|
(get-event-lst 
 '(inv-ds-ds-c1-c2 group-operation-ds-ds-c1-c2 zero-ds-ds-c1-c2 external-ds-ds-c1-c2 inverse-ds-ds-c1-c2 d-ds-ds-c1-c2
   inv-ds-ds-d1-d2 group-operation-ds-ds-d1-d2 zero-ds-ds-d1-d2 external-ds-ds-d1-d2 inverse-ds-ds-d1-d2 d-ds-ds-d1-d2 
   inv-ds-ds-h1-h2 group-operation-ds-ds-h1-h2 zero-ds-ds-h1-h2 external-ds-ds-h1-h2 inverse-ds-ds-h1-h2 d-ds-ds-h1-h2
   lf-ds  lg-ds  lh-ds rf-ds rg-ds rh-ds
   |HOMOTOPY-EQUIVALENCE-DS-is-an-homotopy-equivalence|
   )
 )
|#


(defconst *ds-reduction-theorem*
  '((DEFUN INV-DS-DS-C1-C2 (N A)
        (AND (EQUAL (LIST (CAR A) (CADR A)) A)
             (INV-C1 N (CAR A))
             (INV-C2 N (CADR A))))
 (DEFUN GROUP-OPERATION-DS-DS-C1-C2 (N A B)
        (LIST (GROUP-OPERATION-C1 N (CAR A) (CAR B))
              (GROUP-OPERATION-C2 N (CADR A)
                                  (CADR B))))
 (DEFUN ZERO-DS-DS-C1-C2 (N)
        (LIST (ZERO-C1 N) (ZERO-C2 N)))
 (DEFUN EXTERNAL-DS-DS-C1-C2 (N A B)
        (LIST (EXTERNAL-C1 N A (CAR B))
              (EXTERNAL-C2 N A (CADR B))))
 (DEFUN INVERSE-DS-DS-C1-C2 (N A)
        (LIST (INVERSE-C1 N (CAR A))
              (INVERSE-C2 N (CADR A))))
 (DEFUN D-DS-DS-C1-C2 (N A)
        (LIST (D-C1 N (CAR A))
              (D-C2 N (CADR A))))
 (DEFUN INV-DS-DS-D1-D2 (N A)
        (AND (EQUAL (LIST (CAR A) (CADR A)) A)
             (INV-D1 N (CAR A))
             (INV-D2 N (CADR A))))
 (DEFUN GROUP-OPERATION-DS-DS-D1-D2 (N A B)
        (LIST (GROUP-OPERATION-D1 N (CAR A) (CAR B))
              (GROUP-OPERATION-D2 N (CADR A)
                                  (CADR B))))
 (DEFUN ZERO-DS-DS-D1-D2 (N)
        (LIST (ZERO-D1 N) (ZERO-D2 N)))
 (DEFUN EXTERNAL-DS-DS-D1-D2 (N A B)
        (LIST (EXTERNAL-D1 N A (CAR B))
              (EXTERNAL-D2 N A (CADR B))))
 (DEFUN INVERSE-DS-DS-D1-D2 (N A)
        (LIST (INVERSE-D1 N (CAR A))
              (INVERSE-D2 N (CADR A))))
 (DEFUN D-DS-DS-D1-D2 (N A)
        (LIST (D-D1 N (CAR A))
              (D-D2 N (CADR A))))
 (DEFUN INV-DS-DS-H1-H2 (N A)
        (AND (EQUAL (LIST (CAR A) (CADR A)) A)
             (INV-H1 N (CAR A))
             (INV-H2 N (CADR A))))
 (DEFUN GROUP-OPERATION-DS-DS-H1-H2 (N A B)
        (LIST (GROUP-OPERATION-H1 N (CAR A) (CAR B))
              (GROUP-OPERATION-H2 N (CADR A)
                                  (CADR B))))
 (DEFUN ZERO-DS-DS-H1-H2 (N)
        (LIST (ZERO-H1 N) (ZERO-H2 N)))
 (DEFUN EXTERNAL-DS-DS-H1-H2 (N A B)
        (LIST (EXTERNAL-H1 N A (CAR B))
              (EXTERNAL-H2 N A (CADR B))))
 (DEFUN INVERSE-DS-DS-H1-H2 (N A)
        (LIST (INVERSE-H1 N (CAR A))
              (INVERSE-H2 N (CADR A))))
 (DEFUN D-DS-DS-H1-H2 (N A)
        (LIST (D-H1 N (CAR A))
              (D-H2 N (CADR A))))
 (DEFUN LF-DS (N A)
        (LIST (LF1 N (CAR A)) (LF2 N (CADR A))))
 (DEFUN LG-DS (N A)
        (LIST (LG1 N (CAR A)) (LG2 N (CADR A))))
 (DEFUN LH-DS (N A)
        (LIST (LH1 N (CAR A)) (LH2 N (CADR A))))
 (DEFUN RF-DS (N A)
        (LIST (RF1 N (CAR A)) (RF2 N (CADR A))))
 (DEFUN RG-DS (N A)
        (LIST (RG1 N (CAR A)) (RG2 N (CADR A))))
 (DEFUN RH-DS (N A)
        (LIST (RH1 N (CAR A)) (RH2 N (CADR A))))
 (DEFTHM
  |HOMOTOPY-EQUIVALENCE-DS-is-an-homotopy-equivalence|
  (AND
   (AND
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N))
                (INV-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B)))
       (IMPLIES
        (AND (INV-DS-DS-D1-D2 N A)
             (INV-DS-DS-D1-D2 N B)
             (INV-DS-DS-D1-D2 N C)
             (INTEGERP N))
        (EQUAL
           (GROUP-OPERATION-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                                        C)
           (GROUP-OPERATION-DS-DS-D1-D2
                N
                A (GROUP-OPERATION-DS-DS-D1-D2 N B C))))
       (INV-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A (ZERO-DS-DS-D1-D2 N))
                       A))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (INV-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                            (ZERO-DS-DS-D1-D2 N)))
                (EQUAL (INVERSE-DS-DS-D1-D2 N A) B))
       (IMPLIES
           (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
           (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A (INVERSE-DS-DS-D1-D2 N A))
                  (ZERO-DS-DS-D1-D2 N)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                       (GROUP-OPERATION-DS-DS-D1-D2 N B A)))
       (IMPLIES
        (AND (INV-DS-DS-D1-D2 N A)
             (INV-DS-DS-D1-D2 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL (EXTERNAL-DS-DS-D1-D2 N R (GROUP-OPERATION-DS-DS-D1-D2 N A B))
               (GROUP-OPERATION-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A)
                                            (EXTERNAL-DS-DS-D1-D2 N R B))))
       (IMPLIES
          (AND (INV-DS-DS-D1-D2 N A)
               (INV-RING-Z S)
               (INV-RING-Z R)
               (INTEGERP N))
          (EQUAL (EXTERNAL-DS-DS-D1-D2 N (ADDITION-RING-Z S R)
                                       A)
                 (GROUP-OPERATION-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N S A)
                                              (EXTERNAL-DS-DS-D1-D2 N R A))))
       (IMPLIES
            (AND (INV-DS-DS-D1-D2 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-DS-DS-D1-D2 N (PRODUCT-RING-Z S R)
                                         A)
                   (EXTERNAL-DS-DS-D1-D2 N S (EXTERNAL-DS-DS-D1-D2 N R A))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-D1-D2 N (UNIT-Z) A)
                       A))
       (IMPLIES
           (AND (INV-DS-DS-D1-D2 N A)
                (INV-DS-DS-D1-D2 N B)
                (INTEGERP N))
           (EQUAL (INVERSE-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                  (GROUP-OPERATION-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A)
                                               (INVERSE-DS-DS-D1-D2 N B))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N S A))
                       (EXTERNAL-DS-DS-D1-D2 N S (INVERSE-DS-DS-D1-D2 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
                       (ZERO-DS-DS-D1-D2 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-D1-D2 N S (ZERO-DS-DS-D1-D2 N))
                       (ZERO-DS-DS-D1-D2 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                 (INV-DS-DS-D1-D2 (+ N -1)
                                  (D-DS-DS-D1-D2 N A)))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                      (INV-DS-DS-D1-D2 N B)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                        (GROUP-OPERATION-DS-DS-D1-D2 (+ N -1)
                                                     (D-DS-DS-D1-D2 N A)
                                                     (D-DS-DS-D1-D2 N B))))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A))
                        (EXTERNAL-DS-DS-D1-D2 (+ N -1)
                                              R (D-DS-DS-D1-D2 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
                        (ZERO-DS-DS-D1-D2 (+ N -1))))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A))
                        (INVERSE-DS-DS-D1-D2 (+ N -1)
                                             (D-DS-DS-D1-D2 N A)))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (D-DS-DS-D1-D2 (1- N)
                                      (D-DS-DS-D1-D2 N A))
                       (ZERO-DS-DS-D1-D2 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                     (INV-DS-DS-C1-C2 N B)
                     (INTEGERP N))
                (INV-DS-DS-C1-C2 N (GROUP-OPERATION-DS-DS-C1-C2 N A B)))
       (IMPLIES
        (AND (INV-DS-DS-C1-C2 N A)
             (INV-DS-DS-C1-C2 N B)
             (INV-DS-DS-C1-C2 N C)
             (INTEGERP N))
        (EQUAL
           (GROUP-OPERATION-DS-DS-C1-C2 N (GROUP-OPERATION-DS-DS-C1-C2 N A B)
                                        C)
           (GROUP-OPERATION-DS-DS-C1-C2
                N
                A (GROUP-OPERATION-DS-DS-C1-C2 N B C))))
       (INV-DS-DS-C1-C2 N (ZERO-DS-DS-C1-C2 N))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-DS-DS-C1-C2 N (EXTERNAL-DS-DS-C1-C2 N R A)))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-C1-C2 N A (ZERO-DS-DS-C1-C2 N))
                       A))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                (INV-DS-DS-C1-C2 N (INVERSE-DS-DS-C1-C2 N A)))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                     (INV-DS-DS-C1-C2 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-DS-DS-C1-C2 N A B)
                            (ZERO-DS-DS-C1-C2 N)))
                (EQUAL (INVERSE-DS-DS-C1-C2 N A) B))
       (IMPLIES
           (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
           (EQUAL (GROUP-OPERATION-DS-DS-C1-C2 N A (INVERSE-DS-DS-C1-C2 N A))
                  (ZERO-DS-DS-C1-C2 N)))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                     (INV-DS-DS-C1-C2 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-C1-C2 N A B)
                       (GROUP-OPERATION-DS-DS-C1-C2 N B A)))
       (IMPLIES
        (AND (INV-DS-DS-C1-C2 N A)
             (INV-DS-DS-C1-C2 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL (EXTERNAL-DS-DS-C1-C2 N R (GROUP-OPERATION-DS-DS-C1-C2 N A B))
               (GROUP-OPERATION-DS-DS-C1-C2 N (EXTERNAL-DS-DS-C1-C2 N R A)
                                            (EXTERNAL-DS-DS-C1-C2 N R B))))
       (IMPLIES
          (AND (INV-DS-DS-C1-C2 N A)
               (INV-RING-Z S)
               (INV-RING-Z R)
               (INTEGERP N))
          (EQUAL (EXTERNAL-DS-DS-C1-C2 N (ADDITION-RING-Z S R)
                                       A)
                 (GROUP-OPERATION-DS-DS-C1-C2 N (EXTERNAL-DS-DS-C1-C2 N S A)
                                              (EXTERNAL-DS-DS-C1-C2 N R A))))
       (IMPLIES
            (AND (INV-DS-DS-C1-C2 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-DS-DS-C1-C2 N (PRODUCT-RING-Z S R)
                                         A)
                   (EXTERNAL-DS-DS-C1-C2 N S (EXTERNAL-DS-DS-C1-C2 N R A))))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-C1-C2 N (UNIT-Z) A)
                       A))
       (IMPLIES
           (AND (INV-DS-DS-C1-C2 N A)
                (INV-DS-DS-C1-C2 N B)
                (INTEGERP N))
           (EQUAL (INVERSE-DS-DS-C1-C2 N (GROUP-OPERATION-DS-DS-C1-C2 N A B))
                  (GROUP-OPERATION-DS-DS-C1-C2 N (INVERSE-DS-DS-C1-C2 N A)
                                               (INVERSE-DS-DS-C1-C2 N B))))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-DS-DS-C1-C2 N (EXTERNAL-DS-DS-C1-C2 N S A))
                       (EXTERNAL-DS-DS-C1-C2 N S (INVERSE-DS-DS-C1-C2 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-DS-DS-C1-C2 N (ZERO-DS-DS-C1-C2 N))
                       (ZERO-DS-DS-C1-C2 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-C1-C2 N S (ZERO-DS-DS-C1-C2 N))
                       (ZERO-DS-DS-C1-C2 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                 (INV-DS-DS-C1-C2 (+ N -1)
                                  (D-DS-DS-C1-C2 N A)))
        (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                      (INV-DS-DS-C1-C2 N B)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-C1-C2 N (GROUP-OPERATION-DS-DS-C1-C2 N A B))
                        (GROUP-OPERATION-DS-DS-C1-C2 (+ N -1)
                                                     (D-DS-DS-C1-C2 N A)
                                                     (D-DS-DS-C1-C2 N B))))
        (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-C1-C2 N (EXTERNAL-DS-DS-C1-C2 N R A))
                        (EXTERNAL-DS-DS-C1-C2 (+ N -1)
                                              R (D-DS-DS-C1-C2 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-DS-DS-C1-C2 N (ZERO-DS-DS-C1-C2 N))
                        (ZERO-DS-DS-C1-C2 (+ N -1))))
        (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                 (EQUAL (D-DS-DS-C1-C2 N (INVERSE-DS-DS-C1-C2 N A))
                        (INVERSE-DS-DS-C1-C2 (+ N -1)
                                             (D-DS-DS-C1-C2 N A)))))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                (EQUAL (D-DS-DS-C1-C2 (1- N)
                                      (D-DS-DS-C1-C2 N A))
                       (ZERO-DS-DS-C1-C2 (1- (1- N)))))))
     (AND (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                   (INV-DS-DS-C1-C2 N (LF-DS N A)))
          (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                        (INV-DS-DS-D1-D2 N B)
                        (INTEGERP N))
                   (EQUAL (LF-DS N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                          (GROUP-OPERATION-DS-DS-C1-C2 N (LF-DS N A)
                                                       (LF-DS N B))))
          (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                        (INV-RING-Z R)
                        (INTEGERP N))
                   (EQUAL (LF-DS N (EXTERNAL-DS-DS-D1-D2 N R A))
                          (EXTERNAL-DS-DS-C1-C2 N R (LF-DS N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (LF-DS N (ZERO-DS-DS-D1-D2 N))
                          (ZERO-DS-DS-C1-C2 N)))
          (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                   (EQUAL (LF-DS N (INVERSE-DS-DS-D1-D2 N A))
                          (INVERSE-DS-DS-C1-C2 N (LF-DS N A)))))
     (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
              (EQUAL (D-DS-DS-C1-C2 N (LF-DS N A))
                     (LF-DS (1- N) (D-DS-DS-D1-D2 N A)))))
    (AND (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                  (INV-DS-DS-D1-D2 (+ N 1) (LH-DS N A)))
         (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                       (INV-DS-DS-D1-D2 N B)
                       (INTEGERP N))
                  (EQUAL (LH-DS N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                         (GROUP-OPERATION-DS-DS-D1-D2 (+ N 1)
                                                      (LH-DS N A)
                                                      (LH-DS N B))))
         (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                       (INV-RING-Z R)
                       (INTEGERP N))
                  (EQUAL (LH-DS N (EXTERNAL-DS-DS-D1-D2 N R A))
                         (EXTERNAL-DS-DS-D1-D2 (+ N 1)
                                               R (LH-DS N A))))
         (IMPLIES (INTEGERP N)
                  (EQUAL (LH-DS N (ZERO-DS-DS-D1-D2 N))
                         (ZERO-DS-DS-D1-D2 (+ N 1))))
         (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                  (EQUAL (LH-DS N (INVERSE-DS-DS-D1-D2 N A))
                         (INVERSE-DS-DS-D1-D2 (+ N 1)
                                              (LH-DS N A)))))
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                     (INV-DS-DS-C1-C2 N B)
                     (INTEGERP N))
                (INV-DS-DS-C1-C2 N (GROUP-OPERATION-DS-DS-C1-C2 N A B)))
       (IMPLIES
        (AND (INV-DS-DS-C1-C2 N A)
             (INV-DS-DS-C1-C2 N B)
             (INV-DS-DS-C1-C2 N C)
             (INTEGERP N))
        (EQUAL
           (GROUP-OPERATION-DS-DS-C1-C2 N (GROUP-OPERATION-DS-DS-C1-C2 N A B)
                                        C)
           (GROUP-OPERATION-DS-DS-C1-C2
                N
                A (GROUP-OPERATION-DS-DS-C1-C2 N B C))))
       (INV-DS-DS-C1-C2 N (ZERO-DS-DS-C1-C2 N))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-DS-DS-C1-C2 N (EXTERNAL-DS-DS-C1-C2 N R A)))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-C1-C2 N A (ZERO-DS-DS-C1-C2 N))
                       A))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                (INV-DS-DS-C1-C2 N (INVERSE-DS-DS-C1-C2 N A)))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                     (INV-DS-DS-C1-C2 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-DS-DS-C1-C2 N A B)
                            (ZERO-DS-DS-C1-C2 N)))
                (EQUAL (INVERSE-DS-DS-C1-C2 N A) B))
       (IMPLIES
           (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
           (EQUAL (GROUP-OPERATION-DS-DS-C1-C2 N A (INVERSE-DS-DS-C1-C2 N A))
                  (ZERO-DS-DS-C1-C2 N)))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                     (INV-DS-DS-C1-C2 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-C1-C2 N A B)
                       (GROUP-OPERATION-DS-DS-C1-C2 N B A)))
       (IMPLIES
        (AND (INV-DS-DS-C1-C2 N A)
             (INV-DS-DS-C1-C2 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL (EXTERNAL-DS-DS-C1-C2 N R (GROUP-OPERATION-DS-DS-C1-C2 N A B))
               (GROUP-OPERATION-DS-DS-C1-C2 N (EXTERNAL-DS-DS-C1-C2 N R A)
                                            (EXTERNAL-DS-DS-C1-C2 N R B))))
       (IMPLIES
          (AND (INV-DS-DS-C1-C2 N A)
               (INV-RING-Z S)
               (INV-RING-Z R)
               (INTEGERP N))
          (EQUAL (EXTERNAL-DS-DS-C1-C2 N (ADDITION-RING-Z S R)
                                       A)
                 (GROUP-OPERATION-DS-DS-C1-C2 N (EXTERNAL-DS-DS-C1-C2 N S A)
                                              (EXTERNAL-DS-DS-C1-C2 N R A))))
       (IMPLIES
            (AND (INV-DS-DS-C1-C2 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-DS-DS-C1-C2 N (PRODUCT-RING-Z S R)
                                         A)
                   (EXTERNAL-DS-DS-C1-C2 N S (EXTERNAL-DS-DS-C1-C2 N R A))))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-C1-C2 N (UNIT-Z) A)
                       A))
       (IMPLIES
           (AND (INV-DS-DS-C1-C2 N A)
                (INV-DS-DS-C1-C2 N B)
                (INTEGERP N))
           (EQUAL (INVERSE-DS-DS-C1-C2 N (GROUP-OPERATION-DS-DS-C1-C2 N A B))
                  (GROUP-OPERATION-DS-DS-C1-C2 N (INVERSE-DS-DS-C1-C2 N A)
                                               (INVERSE-DS-DS-C1-C2 N B))))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-DS-DS-C1-C2 N (EXTERNAL-DS-DS-C1-C2 N S A))
                       (EXTERNAL-DS-DS-C1-C2 N S (INVERSE-DS-DS-C1-C2 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-DS-DS-C1-C2 N (ZERO-DS-DS-C1-C2 N))
                       (ZERO-DS-DS-C1-C2 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-C1-C2 N S (ZERO-DS-DS-C1-C2 N))
                       (ZERO-DS-DS-C1-C2 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                 (INV-DS-DS-C1-C2 (+ N -1)
                                  (D-DS-DS-C1-C2 N A)))
        (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                      (INV-DS-DS-C1-C2 N B)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-C1-C2 N (GROUP-OPERATION-DS-DS-C1-C2 N A B))
                        (GROUP-OPERATION-DS-DS-C1-C2 (+ N -1)
                                                     (D-DS-DS-C1-C2 N A)
                                                     (D-DS-DS-C1-C2 N B))))
        (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-C1-C2 N (EXTERNAL-DS-DS-C1-C2 N R A))
                        (EXTERNAL-DS-DS-C1-C2 (+ N -1)
                                              R (D-DS-DS-C1-C2 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-DS-DS-C1-C2 N (ZERO-DS-DS-C1-C2 N))
                        (ZERO-DS-DS-C1-C2 (+ N -1))))
        (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                 (EQUAL (D-DS-DS-C1-C2 N (INVERSE-DS-DS-C1-C2 N A))
                        (INVERSE-DS-DS-C1-C2 (+ N -1)
                                             (D-DS-DS-C1-C2 N A)))))
       (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                (EQUAL (D-DS-DS-C1-C2 (1- N)
                                      (D-DS-DS-C1-C2 N A))
                       (ZERO-DS-DS-C1-C2 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N))
                (INV-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B)))
       (IMPLIES
        (AND (INV-DS-DS-D1-D2 N A)
             (INV-DS-DS-D1-D2 N B)
             (INV-DS-DS-D1-D2 N C)
             (INTEGERP N))
        (EQUAL
           (GROUP-OPERATION-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                                        C)
           (GROUP-OPERATION-DS-DS-D1-D2
                N
                A (GROUP-OPERATION-DS-DS-D1-D2 N B C))))
       (INV-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A (ZERO-DS-DS-D1-D2 N))
                       A))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (INV-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                            (ZERO-DS-DS-D1-D2 N)))
                (EQUAL (INVERSE-DS-DS-D1-D2 N A) B))
       (IMPLIES
           (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
           (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A (INVERSE-DS-DS-D1-D2 N A))
                  (ZERO-DS-DS-D1-D2 N)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                       (GROUP-OPERATION-DS-DS-D1-D2 N B A)))
       (IMPLIES
        (AND (INV-DS-DS-D1-D2 N A)
             (INV-DS-DS-D1-D2 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL (EXTERNAL-DS-DS-D1-D2 N R (GROUP-OPERATION-DS-DS-D1-D2 N A B))
               (GROUP-OPERATION-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A)
                                            (EXTERNAL-DS-DS-D1-D2 N R B))))
       (IMPLIES
          (AND (INV-DS-DS-D1-D2 N A)
               (INV-RING-Z S)
               (INV-RING-Z R)
               (INTEGERP N))
          (EQUAL (EXTERNAL-DS-DS-D1-D2 N (ADDITION-RING-Z S R)
                                       A)
                 (GROUP-OPERATION-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N S A)
                                              (EXTERNAL-DS-DS-D1-D2 N R A))))
       (IMPLIES
            (AND (INV-DS-DS-D1-D2 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-DS-DS-D1-D2 N (PRODUCT-RING-Z S R)
                                         A)
                   (EXTERNAL-DS-DS-D1-D2 N S (EXTERNAL-DS-DS-D1-D2 N R A))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-D1-D2 N (UNIT-Z) A)
                       A))
       (IMPLIES
           (AND (INV-DS-DS-D1-D2 N A)
                (INV-DS-DS-D1-D2 N B)
                (INTEGERP N))
           (EQUAL (INVERSE-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                  (GROUP-OPERATION-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A)
                                               (INVERSE-DS-DS-D1-D2 N B))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N S A))
                       (EXTERNAL-DS-DS-D1-D2 N S (INVERSE-DS-DS-D1-D2 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
                       (ZERO-DS-DS-D1-D2 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-D1-D2 N S (ZERO-DS-DS-D1-D2 N))
                       (ZERO-DS-DS-D1-D2 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                 (INV-DS-DS-D1-D2 (+ N -1)
                                  (D-DS-DS-D1-D2 N A)))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                      (INV-DS-DS-D1-D2 N B)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                        (GROUP-OPERATION-DS-DS-D1-D2 (+ N -1)
                                                     (D-DS-DS-D1-D2 N A)
                                                     (D-DS-DS-D1-D2 N B))))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A))
                        (EXTERNAL-DS-DS-D1-D2 (+ N -1)
                                              R (D-DS-DS-D1-D2 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
                        (ZERO-DS-DS-D1-D2 (+ N -1))))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A))
                        (INVERSE-DS-DS-D1-D2 (+ N -1)
                                             (D-DS-DS-D1-D2 N A)))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (D-DS-DS-D1-D2 (1- N)
                                      (D-DS-DS-D1-D2 N A))
                       (ZERO-DS-DS-D1-D2 (1- (1- N)))))))
     (AND (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                   (INV-DS-DS-D1-D2 N (LG-DS N A)))
          (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                        (INV-DS-DS-C1-C2 N B)
                        (INTEGERP N))
                   (EQUAL (LG-DS N (GROUP-OPERATION-DS-DS-C1-C2 N A B))
                          (GROUP-OPERATION-DS-DS-D1-D2 N (LG-DS N A)
                                                       (LG-DS N B))))
          (IMPLIES (AND (INV-DS-DS-C1-C2 N A)
                        (INV-RING-Z R)
                        (INTEGERP N))
                   (EQUAL (LG-DS N (EXTERNAL-DS-DS-C1-C2 N R A))
                          (EXTERNAL-DS-DS-D1-D2 N R (LG-DS N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (LG-DS N (ZERO-DS-DS-C1-C2 N))
                          (ZERO-DS-DS-D1-D2 N)))
          (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
                   (EQUAL (LG-DS N (INVERSE-DS-DS-C1-C2 N A))
                          (INVERSE-DS-DS-D1-D2 N (LG-DS N A)))))
     (IMPLIES (AND (INV-DS-DS-C1-C2 N A) (INTEGERP N))
              (EQUAL (D-DS-DS-D1-D2 N (LG-DS N A))
                     (LG-DS (1- N) (D-DS-DS-C1-C2 N A)))))
    (IMPLIES (AND (INV-DS-DS-C1-C2 N GNRT)
                  (INTEGERP N))
             (EQUAL (LF-DS N (LG-DS N GNRT)) GNRT))
    (IMPLIES
     (AND (INV-DS-DS-D1-D2 N GNRT)
          (INTEGERP N))
     (EQUAL
         (GROUP-OPERATION-DS-DS-D1-D2 N (LH-DS (1- N) (D-DS-DS-D1-D2 N GNRT))
                                      (D-DS-DS-D1-D2 (1+ N) (LH-DS N GNRT)))
         (GROUP-OPERATION-DS-DS-D1-D2
              N GNRT
              (INVERSE-DS-DS-D1-D2 N (LG-DS N (LF-DS N GNRT))))))
    (IMPLIES (AND (INV-DS-DS-D1-D2 N GNRT)
                  (INTEGERP N))
             (EQUAL (LF-DS (1+ N) (LH-DS N GNRT))
                    (ZERO-DS-DS-C1-C2 (1+ N))))
    (IMPLIES (AND (INV-DS-DS-C1-C2 N GNRT)
                  (INTEGERP N))
             (EQUAL (LH-DS N (LG-DS N GNRT))
                    (ZERO-DS-DS-D1-D2 (1+ N))))
    (IMPLIES (AND (INV-DS-DS-D1-D2 N GNRT)
                  (INTEGERP N))
             (EQUAL (LH-DS (1+ N) (LH-DS N GNRT))
                    (ZERO-DS-DS-D1-D2 (1+ (1+ N))))))
   (AND
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N))
                (INV-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B)))
       (IMPLIES
        (AND (INV-DS-DS-D1-D2 N A)
             (INV-DS-DS-D1-D2 N B)
             (INV-DS-DS-D1-D2 N C)
             (INTEGERP N))
        (EQUAL
           (GROUP-OPERATION-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                                        C)
           (GROUP-OPERATION-DS-DS-D1-D2
                N
                A (GROUP-OPERATION-DS-DS-D1-D2 N B C))))
       (INV-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A (ZERO-DS-DS-D1-D2 N))
                       A))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (INV-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                            (ZERO-DS-DS-D1-D2 N)))
                (EQUAL (INVERSE-DS-DS-D1-D2 N A) B))
       (IMPLIES
           (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
           (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A (INVERSE-DS-DS-D1-D2 N A))
                  (ZERO-DS-DS-D1-D2 N)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                       (GROUP-OPERATION-DS-DS-D1-D2 N B A)))
       (IMPLIES
        (AND (INV-DS-DS-D1-D2 N A)
             (INV-DS-DS-D1-D2 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL (EXTERNAL-DS-DS-D1-D2 N R (GROUP-OPERATION-DS-DS-D1-D2 N A B))
               (GROUP-OPERATION-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A)
                                            (EXTERNAL-DS-DS-D1-D2 N R B))))
       (IMPLIES
          (AND (INV-DS-DS-D1-D2 N A)
               (INV-RING-Z S)
               (INV-RING-Z R)
               (INTEGERP N))
          (EQUAL (EXTERNAL-DS-DS-D1-D2 N (ADDITION-RING-Z S R)
                                       A)
                 (GROUP-OPERATION-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N S A)
                                              (EXTERNAL-DS-DS-D1-D2 N R A))))
       (IMPLIES
            (AND (INV-DS-DS-D1-D2 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-DS-DS-D1-D2 N (PRODUCT-RING-Z S R)
                                         A)
                   (EXTERNAL-DS-DS-D1-D2 N S (EXTERNAL-DS-DS-D1-D2 N R A))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-D1-D2 N (UNIT-Z) A)
                       A))
       (IMPLIES
           (AND (INV-DS-DS-D1-D2 N A)
                (INV-DS-DS-D1-D2 N B)
                (INTEGERP N))
           (EQUAL (INVERSE-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                  (GROUP-OPERATION-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A)
                                               (INVERSE-DS-DS-D1-D2 N B))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N S A))
                       (EXTERNAL-DS-DS-D1-D2 N S (INVERSE-DS-DS-D1-D2 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
                       (ZERO-DS-DS-D1-D2 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-D1-D2 N S (ZERO-DS-DS-D1-D2 N))
                       (ZERO-DS-DS-D1-D2 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                 (INV-DS-DS-D1-D2 (+ N -1)
                                  (D-DS-DS-D1-D2 N A)))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                      (INV-DS-DS-D1-D2 N B)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                        (GROUP-OPERATION-DS-DS-D1-D2 (+ N -1)
                                                     (D-DS-DS-D1-D2 N A)
                                                     (D-DS-DS-D1-D2 N B))))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A))
                        (EXTERNAL-DS-DS-D1-D2 (+ N -1)
                                              R (D-DS-DS-D1-D2 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
                        (ZERO-DS-DS-D1-D2 (+ N -1))))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A))
                        (INVERSE-DS-DS-D1-D2 (+ N -1)
                                             (D-DS-DS-D1-D2 N A)))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (D-DS-DS-D1-D2 (1- N)
                                      (D-DS-DS-D1-D2 N A))
                       (ZERO-DS-DS-D1-D2 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                     (INV-DS-DS-H1-H2 N B)
                     (INTEGERP N))
                (INV-DS-DS-H1-H2 N (GROUP-OPERATION-DS-DS-H1-H2 N A B)))
       (IMPLIES
        (AND (INV-DS-DS-H1-H2 N A)
             (INV-DS-DS-H1-H2 N B)
             (INV-DS-DS-H1-H2 N C)
             (INTEGERP N))
        (EQUAL
           (GROUP-OPERATION-DS-DS-H1-H2 N (GROUP-OPERATION-DS-DS-H1-H2 N A B)
                                        C)
           (GROUP-OPERATION-DS-DS-H1-H2
                N
                A (GROUP-OPERATION-DS-DS-H1-H2 N B C))))
       (INV-DS-DS-H1-H2 N (ZERO-DS-DS-H1-H2 N))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-DS-DS-H1-H2 N (EXTERNAL-DS-DS-H1-H2 N R A)))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-H1-H2 N A (ZERO-DS-DS-H1-H2 N))
                       A))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                (INV-DS-DS-H1-H2 N (INVERSE-DS-DS-H1-H2 N A)))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                     (INV-DS-DS-H1-H2 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-DS-DS-H1-H2 N A B)
                            (ZERO-DS-DS-H1-H2 N)))
                (EQUAL (INVERSE-DS-DS-H1-H2 N A) B))
       (IMPLIES
           (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
           (EQUAL (GROUP-OPERATION-DS-DS-H1-H2 N A (INVERSE-DS-DS-H1-H2 N A))
                  (ZERO-DS-DS-H1-H2 N)))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                     (INV-DS-DS-H1-H2 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-H1-H2 N A B)
                       (GROUP-OPERATION-DS-DS-H1-H2 N B A)))
       (IMPLIES
        (AND (INV-DS-DS-H1-H2 N A)
             (INV-DS-DS-H1-H2 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL (EXTERNAL-DS-DS-H1-H2 N R (GROUP-OPERATION-DS-DS-H1-H2 N A B))
               (GROUP-OPERATION-DS-DS-H1-H2 N (EXTERNAL-DS-DS-H1-H2 N R A)
                                            (EXTERNAL-DS-DS-H1-H2 N R B))))
       (IMPLIES
          (AND (INV-DS-DS-H1-H2 N A)
               (INV-RING-Z S)
               (INV-RING-Z R)
               (INTEGERP N))
          (EQUAL (EXTERNAL-DS-DS-H1-H2 N (ADDITION-RING-Z S R)
                                       A)
                 (GROUP-OPERATION-DS-DS-H1-H2 N (EXTERNAL-DS-DS-H1-H2 N S A)
                                              (EXTERNAL-DS-DS-H1-H2 N R A))))
       (IMPLIES
            (AND (INV-DS-DS-H1-H2 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-DS-DS-H1-H2 N (PRODUCT-RING-Z S R)
                                         A)
                   (EXTERNAL-DS-DS-H1-H2 N S (EXTERNAL-DS-DS-H1-H2 N R A))))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-H1-H2 N (UNIT-Z) A)
                       A))
       (IMPLIES
           (AND (INV-DS-DS-H1-H2 N A)
                (INV-DS-DS-H1-H2 N B)
                (INTEGERP N))
           (EQUAL (INVERSE-DS-DS-H1-H2 N (GROUP-OPERATION-DS-DS-H1-H2 N A B))
                  (GROUP-OPERATION-DS-DS-H1-H2 N (INVERSE-DS-DS-H1-H2 N A)
                                               (INVERSE-DS-DS-H1-H2 N B))))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-DS-DS-H1-H2 N (EXTERNAL-DS-DS-H1-H2 N S A))
                       (EXTERNAL-DS-DS-H1-H2 N S (INVERSE-DS-DS-H1-H2 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-DS-DS-H1-H2 N (ZERO-DS-DS-H1-H2 N))
                       (ZERO-DS-DS-H1-H2 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-H1-H2 N S (ZERO-DS-DS-H1-H2 N))
                       (ZERO-DS-DS-H1-H2 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                 (INV-DS-DS-H1-H2 (+ N -1)
                                  (D-DS-DS-H1-H2 N A)))
        (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                      (INV-DS-DS-H1-H2 N B)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-H1-H2 N (GROUP-OPERATION-DS-DS-H1-H2 N A B))
                        (GROUP-OPERATION-DS-DS-H1-H2 (+ N -1)
                                                     (D-DS-DS-H1-H2 N A)
                                                     (D-DS-DS-H1-H2 N B))))
        (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-H1-H2 N (EXTERNAL-DS-DS-H1-H2 N R A))
                        (EXTERNAL-DS-DS-H1-H2 (+ N -1)
                                              R (D-DS-DS-H1-H2 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-DS-DS-H1-H2 N (ZERO-DS-DS-H1-H2 N))
                        (ZERO-DS-DS-H1-H2 (+ N -1))))
        (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                 (EQUAL (D-DS-DS-H1-H2 N (INVERSE-DS-DS-H1-H2 N A))
                        (INVERSE-DS-DS-H1-H2 (+ N -1)
                                             (D-DS-DS-H1-H2 N A)))))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                (EQUAL (D-DS-DS-H1-H2 (1- N)
                                      (D-DS-DS-H1-H2 N A))
                       (ZERO-DS-DS-H1-H2 (1- (1- N)))))))
     (AND (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                   (INV-DS-DS-H1-H2 N (RF-DS N A)))
          (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                        (INV-DS-DS-D1-D2 N B)
                        (INTEGERP N))
                   (EQUAL (RF-DS N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                          (GROUP-OPERATION-DS-DS-H1-H2 N (RF-DS N A)
                                                       (RF-DS N B))))
          (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                        (INV-RING-Z R)
                        (INTEGERP N))
                   (EQUAL (RF-DS N (EXTERNAL-DS-DS-D1-D2 N R A))
                          (EXTERNAL-DS-DS-H1-H2 N R (RF-DS N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (RF-DS N (ZERO-DS-DS-D1-D2 N))
                          (ZERO-DS-DS-H1-H2 N)))
          (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                   (EQUAL (RF-DS N (INVERSE-DS-DS-D1-D2 N A))
                          (INVERSE-DS-DS-H1-H2 N (RF-DS N A)))))
     (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
              (EQUAL (D-DS-DS-H1-H2 N (RF-DS N A))
                     (RF-DS (1- N) (D-DS-DS-D1-D2 N A)))))
    (AND (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                  (INV-DS-DS-D1-D2 (+ N 1) (RH-DS N A)))
         (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                       (INV-DS-DS-D1-D2 N B)
                       (INTEGERP N))
                  (EQUAL (RH-DS N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                         (GROUP-OPERATION-DS-DS-D1-D2 (+ N 1)
                                                      (RH-DS N A)
                                                      (RH-DS N B))))
         (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                       (INV-RING-Z R)
                       (INTEGERP N))
                  (EQUAL (RH-DS N (EXTERNAL-DS-DS-D1-D2 N R A))
                         (EXTERNAL-DS-DS-D1-D2 (+ N 1)
                                               R (RH-DS N A))))
         (IMPLIES (INTEGERP N)
                  (EQUAL (RH-DS N (ZERO-DS-DS-D1-D2 N))
                         (ZERO-DS-DS-D1-D2 (+ N 1))))
         (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                  (EQUAL (RH-DS N (INVERSE-DS-DS-D1-D2 N A))
                         (INVERSE-DS-DS-D1-D2 (+ N 1)
                                              (RH-DS N A)))))
    (AND
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                     (INV-DS-DS-H1-H2 N B)
                     (INTEGERP N))
                (INV-DS-DS-H1-H2 N (GROUP-OPERATION-DS-DS-H1-H2 N A B)))
       (IMPLIES
        (AND (INV-DS-DS-H1-H2 N A)
             (INV-DS-DS-H1-H2 N B)
             (INV-DS-DS-H1-H2 N C)
             (INTEGERP N))
        (EQUAL
           (GROUP-OPERATION-DS-DS-H1-H2 N (GROUP-OPERATION-DS-DS-H1-H2 N A B)
                                        C)
           (GROUP-OPERATION-DS-DS-H1-H2
                N
                A (GROUP-OPERATION-DS-DS-H1-H2 N B C))))
       (INV-DS-DS-H1-H2 N (ZERO-DS-DS-H1-H2 N))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-DS-DS-H1-H2 N (EXTERNAL-DS-DS-H1-H2 N R A)))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-H1-H2 N A (ZERO-DS-DS-H1-H2 N))
                       A))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                (INV-DS-DS-H1-H2 N (INVERSE-DS-DS-H1-H2 N A)))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                     (INV-DS-DS-H1-H2 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-DS-DS-H1-H2 N A B)
                            (ZERO-DS-DS-H1-H2 N)))
                (EQUAL (INVERSE-DS-DS-H1-H2 N A) B))
       (IMPLIES
           (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
           (EQUAL (GROUP-OPERATION-DS-DS-H1-H2 N A (INVERSE-DS-DS-H1-H2 N A))
                  (ZERO-DS-DS-H1-H2 N)))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                     (INV-DS-DS-H1-H2 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-H1-H2 N A B)
                       (GROUP-OPERATION-DS-DS-H1-H2 N B A)))
       (IMPLIES
        (AND (INV-DS-DS-H1-H2 N A)
             (INV-DS-DS-H1-H2 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL (EXTERNAL-DS-DS-H1-H2 N R (GROUP-OPERATION-DS-DS-H1-H2 N A B))
               (GROUP-OPERATION-DS-DS-H1-H2 N (EXTERNAL-DS-DS-H1-H2 N R A)
                                            (EXTERNAL-DS-DS-H1-H2 N R B))))
       (IMPLIES
          (AND (INV-DS-DS-H1-H2 N A)
               (INV-RING-Z S)
               (INV-RING-Z R)
               (INTEGERP N))
          (EQUAL (EXTERNAL-DS-DS-H1-H2 N (ADDITION-RING-Z S R)
                                       A)
                 (GROUP-OPERATION-DS-DS-H1-H2 N (EXTERNAL-DS-DS-H1-H2 N S A)
                                              (EXTERNAL-DS-DS-H1-H2 N R A))))
       (IMPLIES
            (AND (INV-DS-DS-H1-H2 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-DS-DS-H1-H2 N (PRODUCT-RING-Z S R)
                                         A)
                   (EXTERNAL-DS-DS-H1-H2 N S (EXTERNAL-DS-DS-H1-H2 N R A))))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-H1-H2 N (UNIT-Z) A)
                       A))
       (IMPLIES
           (AND (INV-DS-DS-H1-H2 N A)
                (INV-DS-DS-H1-H2 N B)
                (INTEGERP N))
           (EQUAL (INVERSE-DS-DS-H1-H2 N (GROUP-OPERATION-DS-DS-H1-H2 N A B))
                  (GROUP-OPERATION-DS-DS-H1-H2 N (INVERSE-DS-DS-H1-H2 N A)
                                               (INVERSE-DS-DS-H1-H2 N B))))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-DS-DS-H1-H2 N (EXTERNAL-DS-DS-H1-H2 N S A))
                       (EXTERNAL-DS-DS-H1-H2 N S (INVERSE-DS-DS-H1-H2 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-DS-DS-H1-H2 N (ZERO-DS-DS-H1-H2 N))
                       (ZERO-DS-DS-H1-H2 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-H1-H2 N S (ZERO-DS-DS-H1-H2 N))
                       (ZERO-DS-DS-H1-H2 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                 (INV-DS-DS-H1-H2 (+ N -1)
                                  (D-DS-DS-H1-H2 N A)))
        (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                      (INV-DS-DS-H1-H2 N B)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-H1-H2 N (GROUP-OPERATION-DS-DS-H1-H2 N A B))
                        (GROUP-OPERATION-DS-DS-H1-H2 (+ N -1)
                                                     (D-DS-DS-H1-H2 N A)
                                                     (D-DS-DS-H1-H2 N B))))
        (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-H1-H2 N (EXTERNAL-DS-DS-H1-H2 N R A))
                        (EXTERNAL-DS-DS-H1-H2 (+ N -1)
                                              R (D-DS-DS-H1-H2 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-DS-DS-H1-H2 N (ZERO-DS-DS-H1-H2 N))
                        (ZERO-DS-DS-H1-H2 (+ N -1))))
        (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                 (EQUAL (D-DS-DS-H1-H2 N (INVERSE-DS-DS-H1-H2 N A))
                        (INVERSE-DS-DS-H1-H2 (+ N -1)
                                             (D-DS-DS-H1-H2 N A)))))
       (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                (EQUAL (D-DS-DS-H1-H2 (1- N)
                                      (D-DS-DS-H1-H2 N A))
                       (ZERO-DS-DS-H1-H2 (1- (1- N)))))))
     (AND
      (AND
       (AND
        (AND
         (AND
            (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                          (INV-RING-Z (ADDITION-RING-Z X Y)))
                 (IMPLIES (AND (INV-RING-Z X)
                               (INV-RING-Z Y)
                               (INV-RING-Z Z))
                          (EQUAL (ADDITION-RING-Z (ADDITION-RING-Z X Y)
                                                  Z)
                                 (ADDITION-RING-Z X (ADDITION-RING-Z Y Z)))))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z (ZERO-ELEMENT-Z) X)
                            X))
            (IMPLIES (INV-RING-Z X)
                     (EQUAL (ADDITION-RING-Z X (ZERO-ELEMENT-Z))
                            X))
            (INV-RING-Z (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z (INVERSE-Z X) X)
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (EQUAL (ADDITION-RING-Z X (INVERSE-Z X))
                         (ZERO-ELEMENT-Z)))
         (IMPLIES (INV-RING-Z X)
                  (INV-RING-Z (INVERSE-Z X))))
        (AND (AND (IMPLIES (AND (INV-RING-Z X) (INV-RING-Z Y))
                           (INV-RING-Z (PRODUCT-RING-Z X Y)))
                  (IMPLIES (AND (INV-RING-Z X)
                                (INV-RING-Z Y)
                                (INV-RING-Z Z))
                           (EQUAL (PRODUCT-RING-Z (PRODUCT-RING-Z X Y) Z)
                                  (PRODUCT-RING-Z X (PRODUCT-RING-Z Y Z)))))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z (UNIT-Z) X) X))
             (IMPLIES (INV-RING-Z X)
                      (EQUAL (PRODUCT-RING-Z X (UNIT-Z)) X))
             (INV-RING-Z (UNIT-Z)))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z X (ADDITION-RING-Z Y Z))
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Y)
                                         (PRODUCT-RING-Z X Z))))
        (IMPLIES (AND (INV-RING-Z X)
                      (INV-RING-Z Y)
                      (INV-RING-Z Z))
                 (EQUAL (PRODUCT-RING-Z (ADDITION-RING-Z X Y) Z)
                        (ADDITION-RING-Z (PRODUCT-RING-Z X Z)
                                         (PRODUCT-RING-Z Y Z)))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N))
                (INV-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B)))
       (IMPLIES
        (AND (INV-DS-DS-D1-D2 N A)
             (INV-DS-DS-D1-D2 N B)
             (INV-DS-DS-D1-D2 N C)
             (INTEGERP N))
        (EQUAL
           (GROUP-OPERATION-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                                        C)
           (GROUP-OPERATION-DS-DS-D1-D2
                N
                A (GROUP-OPERATION-DS-DS-D1-D2 N B C))))
       (INV-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-RING-Z R)
                     (INTEGERP N))
                (INV-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A (ZERO-DS-DS-D1-D2 N))
                       A))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (INV-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N)
                     (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                            (ZERO-DS-DS-D1-D2 N)))
                (EQUAL (INVERSE-DS-DS-D1-D2 N A) B))
       (IMPLIES
           (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
           (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A (INVERSE-DS-DS-D1-D2 N A))
                  (ZERO-DS-DS-D1-D2 N)))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-DS-DS-D1-D2 N B)
                     (INTEGERP N))
                (EQUAL (GROUP-OPERATION-DS-DS-D1-D2 N A B)
                       (GROUP-OPERATION-DS-DS-D1-D2 N B A)))
       (IMPLIES
        (AND (INV-DS-DS-D1-D2 N A)
             (INV-DS-DS-D1-D2 N B)
             (INV-RING-Z R)
             (INTEGERP N))
        (EQUAL (EXTERNAL-DS-DS-D1-D2 N R (GROUP-OPERATION-DS-DS-D1-D2 N A B))
               (GROUP-OPERATION-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A)
                                            (EXTERNAL-DS-DS-D1-D2 N R B))))
       (IMPLIES
          (AND (INV-DS-DS-D1-D2 N A)
               (INV-RING-Z S)
               (INV-RING-Z R)
               (INTEGERP N))
          (EQUAL (EXTERNAL-DS-DS-D1-D2 N (ADDITION-RING-Z S R)
                                       A)
                 (GROUP-OPERATION-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N S A)
                                              (EXTERNAL-DS-DS-D1-D2 N R A))))
       (IMPLIES
            (AND (INV-DS-DS-D1-D2 N A)
                 (INV-RING-Z S)
                 (INV-RING-Z R)
                 (INTEGERP N))
            (EQUAL (EXTERNAL-DS-DS-D1-D2 N (PRODUCT-RING-Z S R)
                                         A)
                   (EXTERNAL-DS-DS-D1-D2 N S (EXTERNAL-DS-DS-D1-D2 N R A))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-D1-D2 N (UNIT-Z) A)
                       A))
       (IMPLIES
           (AND (INV-DS-DS-D1-D2 N A)
                (INV-DS-DS-D1-D2 N B)
                (INTEGERP N))
           (EQUAL (INVERSE-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                  (GROUP-OPERATION-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A)
                                               (INVERSE-DS-DS-D1-D2 N B))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                     (INV-RING-Z S)
                     (INTEGERP N))
                (EQUAL (INVERSE-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N S A))
                       (EXTERNAL-DS-DS-D1-D2 N S (INVERSE-DS-DS-D1-D2 N A))))
       (IMPLIES (INTEGERP N)
                (EQUAL (INVERSE-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
                       (ZERO-DS-DS-D1-D2 N)))
       (IMPLIES (AND (INV-RING-Z S) (INTEGERP N))
                (EQUAL (EXTERNAL-DS-DS-D1-D2 N S (ZERO-DS-DS-D1-D2 N))
                       (ZERO-DS-DS-D1-D2 N))))
      (AND
       (AND
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                 (INV-DS-DS-D1-D2 (+ N -1)
                                  (D-DS-DS-D1-D2 N A)))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                      (INV-DS-DS-D1-D2 N B)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (GROUP-OPERATION-DS-DS-D1-D2 N A B))
                        (GROUP-OPERATION-DS-DS-D1-D2 (+ N -1)
                                                     (D-DS-DS-D1-D2 N A)
                                                     (D-DS-DS-D1-D2 N B))))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A)
                      (INV-RING-Z R)
                      (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (EXTERNAL-DS-DS-D1-D2 N R A))
                        (EXTERNAL-DS-DS-D1-D2 (+ N -1)
                                              R (D-DS-DS-D1-D2 N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (D-DS-DS-D1-D2 N (ZERO-DS-DS-D1-D2 N))
                        (ZERO-DS-DS-D1-D2 (+ N -1))))
        (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                 (EQUAL (D-DS-DS-D1-D2 N (INVERSE-DS-DS-D1-D2 N A))
                        (INVERSE-DS-DS-D1-D2 (+ N -1)
                                             (D-DS-DS-D1-D2 N A)))))
       (IMPLIES (AND (INV-DS-DS-D1-D2 N A) (INTEGERP N))
                (EQUAL (D-DS-DS-D1-D2 (1- N)
                                      (D-DS-DS-D1-D2 N A))
                       (ZERO-DS-DS-D1-D2 (1- (1- N)))))))
     (AND (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                   (INV-DS-DS-D1-D2 N (RG-DS N A)))
          (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                        (INV-DS-DS-H1-H2 N B)
                        (INTEGERP N))
                   (EQUAL (RG-DS N (GROUP-OPERATION-DS-DS-H1-H2 N A B))
                          (GROUP-OPERATION-DS-DS-D1-D2 N (RG-DS N A)
                                                       (RG-DS N B))))
          (IMPLIES (AND (INV-DS-DS-H1-H2 N A)
                        (INV-RING-Z R)
                        (INTEGERP N))
                   (EQUAL (RG-DS N (EXTERNAL-DS-DS-H1-H2 N R A))
                          (EXTERNAL-DS-DS-D1-D2 N R (RG-DS N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (RG-DS N (ZERO-DS-DS-H1-H2 N))
                          (ZERO-DS-DS-D1-D2 N)))
          (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
                   (EQUAL (RG-DS N (INVERSE-DS-DS-H1-H2 N A))
                          (INVERSE-DS-DS-D1-D2 N (RG-DS N A)))))
     (IMPLIES (AND (INV-DS-DS-H1-H2 N A) (INTEGERP N))
              (EQUAL (D-DS-DS-D1-D2 N (RG-DS N A))
                     (RG-DS (1- N) (D-DS-DS-H1-H2 N A)))))
    (IMPLIES (AND (INV-DS-DS-H1-H2 N GNRT)
                  (INTEGERP N))
             (EQUAL (RF-DS N (RG-DS N GNRT)) GNRT))
    (IMPLIES
     (AND (INV-DS-DS-D1-D2 N GNRT)
          (INTEGERP N))
     (EQUAL
         (GROUP-OPERATION-DS-DS-D1-D2 N (RH-DS (1- N) (D-DS-DS-D1-D2 N GNRT))
                                      (D-DS-DS-D1-D2 (1+ N) (RH-DS N GNRT)))
         (GROUP-OPERATION-DS-DS-D1-D2
              N GNRT
              (INVERSE-DS-DS-D1-D2 N (RG-DS N (RF-DS N GNRT))))))
    (IMPLIES (AND (INV-DS-DS-D1-D2 N GNRT)
                  (INTEGERP N))
             (EQUAL (RF-DS (1+ N) (RH-DS N GNRT))
                    (ZERO-DS-DS-H1-H2 (1+ N))))
    (IMPLIES (AND (INV-DS-DS-H1-H2 N GNRT)
                  (INTEGERP N))
             (EQUAL (RH-DS N (RG-DS N GNRT))
                    (ZERO-DS-DS-D1-D2 (1+ N))))
    (IMPLIES (AND (INV-DS-DS-D1-D2 N GNRT)
                  (INTEGERP N))
             (EQUAL (RH-DS (1+ N) (RH-DS N GNRT))
                    (ZERO-DS-DS-D1-D2 (1+ (1+ N))))))))))


(make-generic-theory *DS-REDUCTION-THEOREM*)